(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
le(s(x), s(y)) →+ le(x, y)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [x / s(x), y / s(y)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
le(0', y) → true
le(s(x), 0') → false
le(s(x), s(y)) → le(x, y)
quot(x, 0') → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0', 0', 0')
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0', s(v))
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
le(0', y) → true
le(s(x), 0') → false
le(s(x), s(y)) → le(x, y)
quot(x, 0') → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0', 0', 0')
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0', s(v))
Types:
le :: 0':s:quotZeroErro → 0':s:quotZeroErro → true:false
0' :: 0':s:quotZeroErro
true :: true:false
s :: 0':s:quotZeroErro → 0':s:quotZeroErro
false :: true:false
quot :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if2 :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
hole_true:false1_0 :: true:false
hole_0':s:quotZeroErro2_0 :: 0':s:quotZeroErro
gen_0':s:quotZeroErro3_0 :: Nat → 0':s:quotZeroErro
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
le,
quotIterThey will be analysed ascendingly in the following order:
le < quotIter
(8) Obligation:
TRS:
Rules:
le(
0',
y) →
truele(
s(
x),
0') →
falsele(
s(
x),
s(
y)) →
le(
x,
y)
quot(
x,
0') →
quotZeroErroquot(
x,
s(
y)) →
quotIter(
x,
s(
y),
0',
0',
0')
quotIter(
x,
s(
y),
z,
u,
v) →
if(
le(
x,
z),
x,
s(
y),
z,
u,
v)
if(
true,
x,
y,
z,
u,
v) →
vif(
false,
x,
y,
z,
u,
v) →
if2(
le(
y,
s(
u)),
x,
y,
s(
z),
s(
u),
v)
if2(
false,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
u,
v)
if2(
true,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
0',
s(
v))
Types:
le :: 0':s:quotZeroErro → 0':s:quotZeroErro → true:false
0' :: 0':s:quotZeroErro
true :: true:false
s :: 0':s:quotZeroErro → 0':s:quotZeroErro
false :: true:false
quot :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if2 :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
hole_true:false1_0 :: true:false
hole_0':s:quotZeroErro2_0 :: 0':s:quotZeroErro
gen_0':s:quotZeroErro3_0 :: Nat → 0':s:quotZeroErro
Generator Equations:
gen_0':s:quotZeroErro3_0(0) ⇔ 0'
gen_0':s:quotZeroErro3_0(+(x, 1)) ⇔ s(gen_0':s:quotZeroErro3_0(x))
The following defined symbols remain to be analysed:
le, quotIter
They will be analysed ascendingly in the following order:
le < quotIter
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
le(
gen_0':s:quotZeroErro3_0(
n5_0),
gen_0':s:quotZeroErro3_0(
n5_0)) →
true, rt ∈ Ω(1 + n5
0)
Induction Base:
le(gen_0':s:quotZeroErro3_0(0), gen_0':s:quotZeroErro3_0(0)) →RΩ(1)
true
Induction Step:
le(gen_0':s:quotZeroErro3_0(+(n5_0, 1)), gen_0':s:quotZeroErro3_0(+(n5_0, 1))) →RΩ(1)
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) →IH
true
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
le(
0',
y) →
truele(
s(
x),
0') →
falsele(
s(
x),
s(
y)) →
le(
x,
y)
quot(
x,
0') →
quotZeroErroquot(
x,
s(
y)) →
quotIter(
x,
s(
y),
0',
0',
0')
quotIter(
x,
s(
y),
z,
u,
v) →
if(
le(
x,
z),
x,
s(
y),
z,
u,
v)
if(
true,
x,
y,
z,
u,
v) →
vif(
false,
x,
y,
z,
u,
v) →
if2(
le(
y,
s(
u)),
x,
y,
s(
z),
s(
u),
v)
if2(
false,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
u,
v)
if2(
true,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
0',
s(
v))
Types:
le :: 0':s:quotZeroErro → 0':s:quotZeroErro → true:false
0' :: 0':s:quotZeroErro
true :: true:false
s :: 0':s:quotZeroErro → 0':s:quotZeroErro
false :: true:false
quot :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if2 :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
hole_true:false1_0 :: true:false
hole_0':s:quotZeroErro2_0 :: 0':s:quotZeroErro
gen_0':s:quotZeroErro3_0 :: Nat → 0':s:quotZeroErro
Lemmas:
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) → true, rt ∈ Ω(1 + n50)
Generator Equations:
gen_0':s:quotZeroErro3_0(0) ⇔ 0'
gen_0':s:quotZeroErro3_0(+(x, 1)) ⇔ s(gen_0':s:quotZeroErro3_0(x))
The following defined symbols remain to be analysed:
quotIter
(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol quotIter.
(13) Obligation:
TRS:
Rules:
le(
0',
y) →
truele(
s(
x),
0') →
falsele(
s(
x),
s(
y)) →
le(
x,
y)
quot(
x,
0') →
quotZeroErroquot(
x,
s(
y)) →
quotIter(
x,
s(
y),
0',
0',
0')
quotIter(
x,
s(
y),
z,
u,
v) →
if(
le(
x,
z),
x,
s(
y),
z,
u,
v)
if(
true,
x,
y,
z,
u,
v) →
vif(
false,
x,
y,
z,
u,
v) →
if2(
le(
y,
s(
u)),
x,
y,
s(
z),
s(
u),
v)
if2(
false,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
u,
v)
if2(
true,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
0',
s(
v))
Types:
le :: 0':s:quotZeroErro → 0':s:quotZeroErro → true:false
0' :: 0':s:quotZeroErro
true :: true:false
s :: 0':s:quotZeroErro → 0':s:quotZeroErro
false :: true:false
quot :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if2 :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
hole_true:false1_0 :: true:false
hole_0':s:quotZeroErro2_0 :: 0':s:quotZeroErro
gen_0':s:quotZeroErro3_0 :: Nat → 0':s:quotZeroErro
Lemmas:
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) → true, rt ∈ Ω(1 + n50)
Generator Equations:
gen_0':s:quotZeroErro3_0(0) ⇔ 0'
gen_0':s:quotZeroErro3_0(+(x, 1)) ⇔ s(gen_0':s:quotZeroErro3_0(x))
No more defined symbols left to analyse.
(14) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) → true, rt ∈ Ω(1 + n50)
(15) BOUNDS(n^1, INF)
(16) Obligation:
TRS:
Rules:
le(
0',
y) →
truele(
s(
x),
0') →
falsele(
s(
x),
s(
y)) →
le(
x,
y)
quot(
x,
0') →
quotZeroErroquot(
x,
s(
y)) →
quotIter(
x,
s(
y),
0',
0',
0')
quotIter(
x,
s(
y),
z,
u,
v) →
if(
le(
x,
z),
x,
s(
y),
z,
u,
v)
if(
true,
x,
y,
z,
u,
v) →
vif(
false,
x,
y,
z,
u,
v) →
if2(
le(
y,
s(
u)),
x,
y,
s(
z),
s(
u),
v)
if2(
false,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
u,
v)
if2(
true,
x,
y,
z,
u,
v) →
quotIter(
x,
y,
z,
0',
s(
v))
Types:
le :: 0':s:quotZeroErro → 0':s:quotZeroErro → true:false
0' :: 0':s:quotZeroErro
true :: true:false
s :: 0':s:quotZeroErro → 0':s:quotZeroErro
false :: true:false
quot :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
if2 :: true:false → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro → 0':s:quotZeroErro
hole_true:false1_0 :: true:false
hole_0':s:quotZeroErro2_0 :: 0':s:quotZeroErro
gen_0':s:quotZeroErro3_0 :: Nat → 0':s:quotZeroErro
Lemmas:
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) → true, rt ∈ Ω(1 + n50)
Generator Equations:
gen_0':s:quotZeroErro3_0(0) ⇔ 0'
gen_0':s:quotZeroErro3_0(+(x, 1)) ⇔ s(gen_0':s:quotZeroErro3_0(x))
No more defined symbols left to analyse.
(17) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
le(gen_0':s:quotZeroErro3_0(n5_0), gen_0':s:quotZeroErro3_0(n5_0)) → true, rt ∈ Ω(1 + n50)
(18) BOUNDS(n^1, INF)